COMMENT ⊗   VALID 00006 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	.require "memo.pub[let,jmc]" source
C00006 00003	Here is a predicate that says that the predicate P1 precedes
C00007 00004		The programming language Lucid (Ashcroft 1974 ...) has as
C00008 00005
C00010 00006	∂30-Mar-79  1348	JMC  	elephants
C00020 ENDMK
C⊗;
.require "memo.pub[let,jmc]" source
.cb THE PROGRAMMING LANGUAGE ELEPHANT


	The programming language Elephant (it never forgets)
is a sequential language (i.e. based on assignments).
Its statements may refer to the past of the computation.
For the time being, consider it as an extension to the Lisp program
feature.  Thus statements may refer to

.item←0
	#. x = 3 more recently than y = 9

	#. the value of x the last time y = 3

	Such things can be accomplished by adding to
a simple sequential language a reserved identifier called %2history%1.
Programs can refer to %2history%1 but cannot assign to it.
%2history%1 is a record of all assignments that have been made, i.e. it
is a list of pairs (<variable>.<value>), and it is updated every time
an assignment is made.  The update is made by %2cons%1ing latest
variable-value pair on the front of %2history%1.  Thus the statement

	%2x ← 3%8x%2 + y;%1

would be equivalent to the pair of statements

	%2x ← 3%8x%2 + y; history ← [X . x] . history%1;

in program feature Lisp.

	A good compiler for Elephant will not generate machine code that
maintains an actual %2history%1 variable, because its use would fill up
storage rapidly and searching it would take excessive time.  Instead the
compiler will cleverly decide what information must actually be kept and
generate code that refers to additional variables, arrays, trees and lists
as convenient and required in order to execute the Elephant program.  How
much cleverness is required and whether the modes of reference to the past
have to be restricted or whether the compiler has to be helped remain to
be seen.

	It looks as though one might be able to eliminate assignments
entirely by referring to ⊗history in ever more complex ways.  However,
these more complex ways would involve recursively defined functions,
and variables would creep back in as arguments to these functions.
Moreover, this would probably place excessive burdens on the intelligence
of the compiler which is required to determine what historical
information actually must be preserved.  Therefore we will let variables
and arrays and will merely try to see what is the most natural and
convenient way of writing.  If ⊗history is never referred to, then
Elephant will have turned into a mouse.

	Let us give a simple program in Elephant.

Here is a predicate that says that the predicate ⊗P1 precedes
the predicate ⊗P2 in history

	%2prec(P1,P2,h) ← not qn h and not P2 qa h and (P1 qa h:
or prec(P1,P2,qd h)%1
	The programming language Lucid (Ashcroft 1974 ...) has as
one of its objectives to make the statements of a programming
language sentences of logic interpretable in the ordinary way.
Here is another way of doing it, more straightforward than that
of Lucid, permitting a direct translation of the statements of
a sequential programming language such as Algol 60.

	Consider the following Algol 60 fragment; it lacks declarations.

.begin nofill
%2

	n ← n0; p ← 0;
loop:	qif n = 0 qthen qgo done;
	n ← n - 1; p ← p + m;
	qgo loop;
done:
%1
∂30-Mar-79  1348	JMC  	elephants
To:   FB
CC:   SSO    
I have made considerable progress on Elephant including
	(1) a new formulation in which the statements are true logical
sentences but much simpler than Lucid and admitting a trivial
translation from programs with assignments and go to s.
	(2) A straightforward expression of a reservation system
in which the database is implicit, as was the goal of elephant.
	(3) An example of a correctness proof in first order logic.

There are still large questions about
	(1) Whether parallel programs can be treated using a separate
"local time" for each process.
	(2) The proper concept of equivalence of Elephant programs.

The general idea involves replacing a program like

	n ← n0; p ← 0;
loop:	if n = 0 then go to done;
	n ← n -1; p ← p + m;
	go to loop;
done:

by the sentences

∀t.[n(t+1) =	if pc(t) = 0 then n0
		else if pc(t) = 1 ∧ n(t) ≠ 0 then n(t) - 1
		else n(t)]

∀t.[p(t+1) =	if pc(t) = 0 then 0
		else if pc(t) = 1 ∧ n(t) ≠ 0 then p(t) + m
		else p(t)]

∀t.[pc(t+1) = if pc(t) = 1 ∧ n(t) ≠ 0 then 1 else pc(t) + 1]

from which we can easily prove

pc(0) = 0 ⊃ ∀n0 m.∃t.[pc(t) = 2 ∧ p = m n0]

which expresses the correctness of this program for multiplication
by successive addition.  These sentences are obtained from the sequential
program by (1) introducing an explicit time variable t taking integer
values, (2) representing the position in the program by the value of
the variable pc ("program counter").

In the translation of an ordinary sequential program, the expression for x(t+1) 
will involve only the values of variables at time t.  The extension to
implicit data bases (i.e. Elephant) is obtained by allowing any earlier
values of the time.  This allows the reservation program to say that
a passenger has a reservation if he has successfully made one and
and not subsequently cancelled it without saying what data structures
have to be kept.
I have written it out on paper but want to revise it.

Since you both expressed interest, I would be glad to get together
at a mutually agreeable time.  Your opinions would be interesting,
and maybe you would have suggestions on the open questions.